﻿using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text;
using DFSGenerator;

namespace DFAToCNF
{
    public class Converter : IConvertor
    {
        private IDFA dfa;
        private int c;
        private int beginFirstVar;
        private int beginSecondVar;

        static int NumberOfVariable(int c, int pointNumber)
        {
            var firstTypeVariable = c + 1;
            var secondTypeVariavle = (c + 1) * pointNumber;
            return firstTypeVariable + secondTypeVariavle;
        }

        static int NumberOfClouse(int c, int pointNumber)
        {
            var firstTypeClouse = pointNumber;
            var secondTypeClouse = pointNumber * (c + 1) * 2;
            var thirthTypeClouse = (pointNumber*pointNumber) - pointNumber;
            return firstTypeClouse + secondTypeClouse + thirthTypeClouse;
        }

        public string GetCNF(IDFA dfa, int c)
        {
            var returned = new StringBuilder();
            this.dfa = dfa;
            this.c = c;

            beginFirstVar = 0;
            beginSecondVar = (c + 1);
            var pNum = dfa.pointNumber;

            returned.AppendFormat("c {0}\r\n","Experiment");
            returned.AppendFormat("p cnf {0} {1}\r\n", NumberOfVariable(c, pNum), NumberOfClouse(c, pNum));
            returned.Append(generateFirstClause());
            returned.Append(generateSecondClause());
            returned.Append(generateThirthClause());
            return returned.ToString();
        }

        static int genXq0 (int c, int q)
        {
            return (c + 1)*q;
        }

        StringBuilder generateFirstClause()
        {
            var returned = new StringBuilder();
            returned.AppendFormat("c {0}\r\n", "First type clause!");
            for (int q = 1; q <= dfa.pointNumber; q++)
            {
                returned.AppendFormat("{0} 0\r\n", beginSecondVar + genXq0(c,q));
            }
            return returned;
        }

        static class TwoDisjunction
        {
            static public int GenXqt(int c, int t, int q)
            {
                return (c + 1)*q + t;
            }
            static public int GenUt(int t)
            {
                return t;
            }

            static public int GenXqnt1(int c, int t, int qn)
            {
                var qa = (c + 1)*qn;
                var t1 = (t + 1)%(c + 1);
                return qa + t1;
            }
        }

        StringBuilder generateSecondClause()
        {
            var returned = new StringBuilder();
            returned.AppendFormat("c {0}\r\n", "Second type clause!");
            for (int q = 1; q <= dfa.pointNumber; q++)
            {
                for (int t = 1; t <= c; t++)
                {
                    returned.AppendFormat("-{0} -{1} {2} 0\r\n", beginSecondVar + TwoDisjunction.GenXqt(c, t, q), beginFirstVar + TwoDisjunction.GenUt(t), beginSecondVar + TwoDisjunction.GenXqnt1(c, t, dfa.func[q]["a"]));
                    returned.AppendFormat("{0} {1} {2} 0\r\n", beginSecondVar + TwoDisjunction.GenXqt(c, t, q), beginFirstVar + TwoDisjunction.GenUt(t), beginSecondVar + TwoDisjunction.GenXqnt1(c, t, dfa.func[q]["b"]));
                }
            }
            return returned;
        }

        static class ThreeDisjunction
        {
            static public int GenXqc(int c, int q)
            {
                return q * (c + 1) + c;
            }
            static public int GenXpc(int c, int p)
            {
                return p * (c + 1) + c;
            }
        }


        StringBuilder generateThirthClause()
        {
            var returned = new StringBuilder();
            returned.AppendFormat("c {0}\r\n", "Thirth type clause!");
            for (int p = 1; p <= dfa.pointNumber; p++)
            {
                for (int q = 1; q <= dfa.pointNumber; q++)
                {
                    if (p != q)
                    {
                        returned.AppendFormat("-{0} -{1} 0\r\n", ThreeDisjunction.GenXqc(c,q), ThreeDisjunction.GenXpc(c,p));
                    }
                }
            }
            return returned;
        }
    }
}
